L:System List.
(A,BL.A || B)
 {(L)  System & (M:System. (BL. M || B)  M || (L)) & (BL. B  (L))} 

latex

Definitions	P  Q, P  Q, P  Q, A  B, x:A. B(x), A & B, , (x  l), Dsys, (L), x. t(x), l[i], {i..j}, i  j < k, AB, P & Q, A, False, xL. P(x), D1  D2, , System, {T}, P  Q, (x,yL.P(x;y)), x,y. t(x;y), MsgA, Id, Feasible(M), Prop, A || B, x:A. B(x), t  T
Lemmas	m-sys-compatible wf, ma-feasible wf, msga wf, Id wf, pairwise wf, msystem wf, int seg wf, l all wf, m-sys-null wf, m-sys-null-compatible-right, l member wf, m-sys-join wf, pairwise-cons, cons member, m-sys-compatible-join, m-sys-sub-join-left, m-sys-join wf2, d-sub wf, l all cons, m-sys-sub-join-right, d-sub transitivity